Skip to main content

Full text of "Knots as processes: a new kind of invariant"

See other formats

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

y—( Knots as processes: a new kind of invariant 


L.G. Meredith and David F. Snyder 

rf\ Partner, Bio similarity LLC 

505 N72nd St, Seattle, WA 98103, USA, 
C Igreg. meredith@bio similarity . com 


■i— > 

Department of Mathematics 
Texas State University — San Marcos 
601 University Drive 
San Marcos, TX 78666 
dsnyder&txstate. edu 


We exhibit an encoding of knots into processes in the 7r-calculus such that knots are 
ambient isotopic if and only their encodings are weakly bisimilar. 

^ Keywords: Process calculi, knots, invariants 


1. Introduction 


Knot and link tabulation continues to be a lively area of scientific research and 
promises to be useful to areas of science such as quantum computing and DNA 
unpacking [22] [32] [H]. The past 20 years have seen major advances in knot clas- 
. . sification, the development of knot invariants, and computational methods for tab- 

# ^ ulating knots and links. There are tables of the alternating prime knots of up to 

23 crossings [25] [5T] [52] [27]. While current algorithms provide complete tables of 
knots (and links), winnowing these tables of duplicates is a time consuming task. 
Moreover, as knot tables have proved of use to researchers in genetics, and may 
prove to be to researchers in quantum computation, the need to search these ta- 
bles in meaningful ways presents itself. For example, of the 4,976,016,485 prime, 
non-oriented, alternating knots with minimal crossing number of 22, which contain 
the tangle corresponding to 5/3 (if any)? Of course, knot invariants are useful to 
distinguish knots, but few provide the basis for a formal language of knot properties 
with which to identify classes of knots via logical expressions in the language. 

1.1. Summary of contributions and outline of paper 

Here we present a newly-found strong knot invariant that does give rise to such a 
formal language of knot properties. Knots are invariantly associated to expressions 
in Milner's 7r-calculus [45], a member of a family of dynamic calculi known as the 


September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

mobile process calculi. These calculi were developed for the analysis of concurrent 
computation |46j [56] . The invariant introduced here interprets knot equivalence up 
to ambient isotopy as an equivalence of process dynamics known as bisimulation 
[59] [57] in the concurrency theory literature. Of critical importance, and somewhat 
surprisingly, these two notions of equivalence correspond exactly on the image of 
the encoding: the main result of this paper is that two knots are ambient isotopic 
if, and only if, their images under the encoding are weakly bisimilar. 

Building on this result, we observe that dual to the process calculi are a family 
of logics, the Hennessy-Milner logics (HMLs), providing a logical language capable 
of the classification of processes via logical properties. Factoring this capability 
through our encoding leads to the development of a logical language identifying 
classes of knots with logical properties. In particular, the spatial logics discovered by 
Caires and Cardelli [9] constitute a particularly interesting sub-family of the HMLs 
having logical connectives enabling us to take full advantage of key features of our 
encoding. We illustrate the application of the logic in [5] primarily via examples of 
predicates that select features of knots. 

The paper is organized as follows. First, we provide a brief overview of knot 
presentations relevant to this paper, given in the context of the history of knot 
tabulation. Next, we give a brief overview of process calculi, highlighting achieve- 
ments in that field pertinent to this paper. Section [4] begins the technical exegesis 
with an introduction to Milner's polyadic 7r-calculus via demonstration of process 
expressions that, much like the combinators of Conway's tangle calculus, reflect 
aspects of knot structure (crossings etc.). The section concludes with an example 
encoding of the trefoil knot. Section |4.5| gives a condensed but complete formal 
presentation of the process calculus. The main theorem is proved in section [5] This 
is followed by an account of spatial logic via knots in section [6] and how this can be 
applied in the study and inquiry of knot tables, with potential application in knot 
tabulation algorithms themselves. Finally, new techniques are judged not solely by 
the questions they answer but by the new questions to which they give rise. In the 
conclusion, we identify areas of further investigation. 

2. A summary of knot presentations 

The knot presentations we focus upon herein are the Gauss code [53], the Dowker- 
Thistlethwaite (DT) code [17], the Conway notation [15], and the Master Code of 
Rankin, Schcrmann and Smith [51] [52j . Other presentation schemes, such as braid 
representatives and Morse links, are not directly useful to the development of this 
paper and thus are overlooked. We also give a "wish-list" of properties one would 
desire from one's knot notation scheme. 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

2.1. Knot presentations 

This section briefly discusses various knot notations and establishes some terminol- 
ogy, with references for readers needing further details. 

2.1.1. Regular knot projections 

In 1847, J.B. Listing classified knots up to 5 crossings by analyzing knot projections 
[33| . Listing was the first to publish an article containing a drawing of a regular knot 
projection (or knot diagram or planar diagram). A knot is taken to be a polygonal 
simple closed curve in 3-space. Choose any plane on which projection onto the plane 
results in a curve whose only singularities are transverse double points which are 
not the image of any vertex from the polygonal curve. Using a canonical normal 
vector to the plane for line of sight, for a given double point d we find the point c 
in the projection's preimage of d farthest from our line of sight, and we indicate an 
undercrossing by erasing the image of a small neighborhood of c from the planar 
projection. A careful presentation is given in |37j . 

Out of all possible regular projections of a knot, there is (at least) one with 
minimal number of crossings. 

2.1.2. The Gauss code. 

Gauss used regular knot projections to arrive at what is now called the Gauss Code 
of a knot 53]. The Gauss code is the first knot notation system. P. G. Tait used 
an encoding in the 1870's to classify knots up to 7 crossings [63]. Tait's encoding 
may be regarded as an extension to the Gauss Code. One begins somewhere on the 
knot projection (not at a crossing point), then proceeds along the knot applying 
labels to the first, third, fifth etc. crossing until all crossings are labeled; one then 
traverses the knot once more, writing the label of each crossing in the order that 
you reach it, attaching a plus or minus sign, depending on whether you are crossing 
over or under. 

2.1.3. Tait, Little, and Kirkman. 

Using Kirkman's classification of certain polygons [3D], Tait (and Little, using sim- 
ilar methods) was able to tabulate knots up to 11 crossings [53] [33] [33] [35J. Tait's 
system included using a simple reduction rewrite strategy within his notation sys- 
tem. This notation was improved by Dowker and Thistlethwaite, as discussed in 
some detail below. 

2.1.4. Reidemeister moves. 

Rcidcmcistcr developed a reduction rewrite system for knot projections (the three 
Reidemeister moves) [55]. We illustrate the three moves. The convention in these 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

(and in other graphically-based invariants) is that we show only the relevant part 
of the knot. In our diagrams here, we have placed dashed circles, which the reader 
should imagine as viewing through scope lens only a portion of the knot, with the 
remainder of the knot outside of the scope of view and unchanged. 

S> - € 

Fig. 1. The three Reidemeister moves. The topmost move will be referred to as Ri, the middle 
one as R2, and the bottommost as R3. For any one of these moves R, we write R~^(K) (resp. 
R*~(K)) if the move has been applied left-to-right (resp. right-to-left) to the knot diagram K. 

The import of this system is Reidemeister's Theorem: an ambient isotopy of 
two knots may be exhibited as sequences of rewrites of (any of) their diagrams, and 
vice versa. That is, two knots are ambient isotopic if and only if a diagram of one 
may be rewritten, via a sequence of Reidemeister moves, to a diagram of the other 

2.1.5. Knotation 

Conway developed a clever notational system for tangles, finding an algebraic-like 
system for this system that led to several methods of reduction rewrites |15j . He used 
this system to retabulate knots and links of 11 crossings by hand, in one afternoon 
(an effort that took Tait and Little years of work), discovering one omission and 
a few duplications in the process. Conway's system can be used to classify all 
arithmetic (also called algebraic, or rational) knots. The Conway code for a knot 
originally was given as a basic polyhedron followed by a sorted list of arithmetic 
tangles. See Conway's paper [TS] for details. This system has extensions by Caudron 
[T4"] and by Bangert [5]. Conway has investigated further structures such as bangles 
and bracelets. 

2.1.6. Dowker-Thistlethwaite Codes (DT codes) 

Dowker created a variation of Tait's notational system that is easier to implement 
computationally. Dowker and Thistlethwaite made it the basis for an algorithm 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

that successfully enumerated knots of up to 13 crossings [T7]- Not every DT code 
is valid, i.e. an arbitrary DT code may not correspond to an actual knot, and 
two distinct composite knots may share the same DT Code. However, a valid DT 
code for a prime knot specifies the knot uniquely |61j . In their paper, Dowker and 
Thistlethwaite develop an algorithm to filter out invalid cases. They also give a 
reduction system to remove duplicates from their enumeration. 

We now recall the definition of the DT code of a regular knot projection [17]. 
Begin at a selected point on the diagram (excepting crossing points) and traverse the 
diagram in a selected direction. At each encounter of a crossing, label the crossing 
with the next available counting number; for an even label, prepend a negative sign 
if traversing the overcross. Returning to the beginning point, each crossing has been 
labeled twice, once with an odd number and once with an even number. Let S± 
denote the set of labels generated. 

If the knot projection has n crossings, then there are 2n labels (from 1 to 2n in 
absolute value) and at each crossing an unique odd counting number paired with an 
even integer. This induces a parity-reversing function <r on S = {1, . . . , 2n}, where 
for each i 6 S we find the crossing with label whose absolute value is i and let 
a(i) be the absolute value of the other label at that crossing. Note that a(a(i)) = i 
for any i € S. Note that there is also a bijective translation r : S — > S± where 
\t(s) \ = s for all s 6 S. Then the DT code of the knot projection is determined by 
S = t o a, usually given as the list {S(l), 5(3), . . . , 5(2n — 1)}. Note that 6 o a = t. 
Finally, for each i G S, let sgn(i) denote the sign of r(i) (so sgn(i) < implies i is 
even) . 

For each i 6 S±, let C(i) denote the crossing with label i. Then for any i € S 
we know C(i) is adjacent to the two crossings C(i ± 1) and C(8(i) ± 1)), where 
addition is modulo 2n. This fact is applied later when giving an explicit algorithm 
for encoding a knot. 

2.1.7. From Calvo to Rankin, Flint, and Schermann 

Calvo developed an inductive knot tabulation algorithm, thereby sidestepping the 
need to check validity of DT codes [H] . However, detection of duplication within the 
tables generated then becomes the issue. Calvo had the insight that understanding 
the deeper flype structure of prime, non-alternating diagram led to greater efficien- 
cies in his algorithm. The Calvo algorithm was essentially refined in the development 
of a notational system by Rankin, Flint, and Schermann , based on what they call 
the group code which reminds one somewhat of the Gauss code but, instead, using 
a Conway-likc insertion scheme to allow for easy reduction of flype structures in 
the notation [51] [52] [50]. This results in a master array that provides a unique 
identifier for prime alternating knots. This forms part of the basis for inductive 
construction of all prime alternating knots of crossing size n from those of crossing 
size n — l(see the above papers for details). Composite knots remain problematic, 
due principally to the issue of detection of duplicates. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

2.2. Desirable properties for a knot presentation system 

In this section, we list some properties that one would wish for a knot presenta- 
tion system to enjoy, followed by a discussion of the knot presentations of the last 
subsection in the light of these wishes. 

Due to complexity considerations, one may well despair of a knot notation sys- 
tem that would allow for mathematical classification of all knots. However, in de- 
signing a system of knot notation or presentation, informed by the history of knot 
tabulation and classification we can enumerate the following properties such a no- 
tation system may enjoy. These properties invariably correspond to demands of 
functoriality on the encoding when considered as a map from the category of knots 
or braids to some suitable target category while others are demands on the faith- 
fulness (respectively, fullness) of the encoding considered as functor. 

• Surjection (realizability) . Each code in the notation represents a knot (or 
if this is not the case, those codes that do not represent a knot are easily 
recognizable). A code for a knot should be easily obtained from one of its 
planar diagrams. 

• Reduction. The notation enjoys a calculus with which to reduce and sim- 
plify encodings. Each step of simplification or reduction results in an en- 
coding representing a knot isotopy equivalent to the originating knot. 

• Minimality. The notational encoding of a given knot can be reduced to a 
(finite non-empty set of equivalent) minimal encoding(s). 

• Well-definedness. If a knot has two (or more) minimal reduced encodings, 
each of these encodings is equivalent to the notation for a knot equivalent 
via ambient isotopy to the original. 

• Injection. Two knots that have equivalent minimal reduced encodings are 
ambient isotopic. 

• Economy. The notation is computationally cheap and easily constructed 
from a diagram of the knot or from a simple code, such as the DT code. 

• Compositionality. Operations on knots, e.g. knot composition, correspond 
to natural operations on elements in the image of the encoding. 

• Separation. The notation can be used to classify a class X of knots, where 
X contains a previously classified class of knots (for example, arithmetic 
knots (also known as algebraic knots) and bracelets) but is not previously 
classified itself. 

• Extensibility. The notation enjoys a formal language in which to describe 
properties and invariants of notation objects that reflect interesting proper- 
ties of knots. This language should also be useful in selecting specific sets of 
knots (such as the set of all 21-crossing prime alternating links containing 
the tangle 5/3). This language ideally should be scaleable and be applicable 
to tables of indefinite size. 

The DT code, with proper care taken, satisfies the first six properties but breaks 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

under compositionality. Conway's tangle notation enjoys all of the properties listed, 
though the Conway encoding requires foreknowledge of the classes of basic polygons 
with n vertices. The master array of Rankin, Flint, and Schermann satisfies the first 
five properties, but appears unlikely to support the last four properties to a degree 
useful for anything other than tabulation. 

2.2.1. A meta-knotation 

Due to Reidemeister's Theorem, in order to establish our main theorem we need 
only consider diagrams of knots and not knots themselves. Hence we adopt the 
following convenient notation and terminology. The meta-variable K ranges over 
knot diagrams and we reserve K, to range over knots. For simplicity, we refer to K 
as a knot. We write ifc(K) to mean the number of crossing points in the diagram 
K but will call this value the crossing number of the knot K, which the reader 
is asked not to confuse with the minimal crossing number of the knot (it is in 
this sense that we will later say that "two knots from the same isotopy class can 
have different crossing numbers"). Formally speaking ~; so will denote equivalence 
of knots under ambient isotopy and will denote equivalence of diagrams under 
(finite) sequences of Reidemeister transforms. However, when there is little chance 
of confusion we drop the subscript and write ~. 

3. Concurrent process calculi and spatial logics 

In the last thirty years the process calculi have matured into a remarkably power- 
ful analytic tool for reasoning about concurrent and distributed systems. Process- 
calculus-based algebraical specification of processes began with Milner's Calculus 
for Communicating Systems (CCS) [33] and Hoare's Communicating Sequential 
Processes (CSP) [23J [7] [35] [53], and continue through the development of the 
so-called mobile process calculi, e.g. Milner, Parrow and Walker's 7r-calculus [4"5] . 
Cardelli and Caires's spatial logic (TUJ [3] [5J, or Meredith and Radestock's reflective 
calculi [3D] [31] . The process-calculus-based algebraical specification of processes has 
expanded its scope of applicability to include the specification, analysis, simulation 
and execution of processes in domains such as: 

• telecommunications, networking, security and application level protocols 

n m ED ED; 

• programming language semantics and design [35] [5T] [2U] [B"4"] : 

• webservices [28] [31] [39] : 

• and biological systems [13] [16] [54] [49] . 

Among the many reasons for the continued success of this approach are two 
central points. First, the process algebras provide a compositional approach to the 
specification, analysis and execution of concurrent and distributed systems. Owing 
to Milner's original insights into computation as interaction [44], the process calculi 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

are so organized that the behavior — the semantics — of a system may be composed 
from the behavior of its components [19] . This means that specifications can be 
constructed in terms of components — without a global view of the system — and 
assembled into increasingly complete descriptions. 

The second central point is that process algebras have a potent proof principle, 
yielding a wide range of effective and novel proof techniques [47] [56] [57] [58]. In 
particular, bisimulation encapsulates an effective notion of process equivalence that 
has been used in applications as far-ranging as algorithmic games semantics [3] and 
the construction of model-checkers [8j. The essential notion can be stated in an 
intuitively recursive formulation: a bisimulation between two processes P and Q is 
an equivalence relation E relating P and Q such that: whatever action of P can be 
observed, taking it to a new state P' , can be observed of Q, taking it to a new state 
Q' , such that P' is related to Q' by E and vice versa. P and Q are bisimilar if there 
is some bisimulation relating them. Part of what makes this notion so robust and 
widely applicable is that it is parameterized in the actions observable of processes 
P and Q, thus providing a framework for a broad range of equivalences and up-to 
techniques [32] all governed by the same core principle [5B] [57] [58] . 

4. Knots as processes 

This section bootstraps intuitions about the target calculus by introducing process 
expressions for key aspects of a knot's structure. An n crossing knot K is modeled as 
a system \K\ of concurrently executing processes. More specifically, \K\ is a parallel 
composition n" = r 1 [C(z)]|M / of n + 1 processes consisting of n crossing processes 
[C(i)J and a process W constituting a "wiring harness." The latter process can 
be thought of as the computational equivalent to Conway's "basic polygon," if the 
knot is in minimal crossing number form. The complete expression of the encoding 

IK] := {v ...v 4n ^)(Ilf- x (p u)[C(»)](«4i,...,«4i+3,«) 

\n?=oW{v u ^ fi) ,v U ( iA) )\w(v U ( it 2),v U ( it3) )) 

Here, C(i) represents the ith crossing in the knot diagram K. The wiring process, 
n2r 1 W'(u w (i ) o),«u)(t,i))l^ r ( 1; «(t,2)» t 'w(t,3))) is itself a parallel composition of wire pro- 
cesses that correspond to edges in the 4-valent graph of the knot shadow [61] the 
constraints of which are reflected in the indexing function u>. The wiring process 
may be calculated from other knot notations. For example, we later show how the 
indexing function uj may be calculated from S, the DT code of the knot projection. 
The crossing and wire processes have further substructure, outlined below. 

Remark 4.1 (knots as abstractions). The reader familiar with process calculi 
will observe that the encoding actually produces an abstraction [56 in A^j={K) 
names (see the first choice in the production labeled agent in the grammar of |4.5[). 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

This is actually a way of demarking that the encoding should be insensitive to the 
particular set of names chosen to represent the ports of the crossings. Some caution 
must be exercised, however, as the encoding only preserves knot structure if the 
abstraction is applied to a vector of A#(K) distinct names. 

4.1. Crossing processes 

A crossing is conceived in the diagram below as a black-box having four points of 
external interaction (ports) with the remainder of the knot process and as having 
two internal wires each connecting a pair of ports. As a process, the crossing has 
four possible behaviors, as shown in the defining encoding below. 

yo yr 

Fig. 2. Crossing process 

C(x ,x 1 ,y Q ,y 1 ,u) <- x 1 ?(s).y l(s).(C(x ,x 1 ,y ,y 1 ,u)\ul) 
+yo?(s).x 1 l(s).(C(x ,x 1 ,y ,y 1 ,u)\ul) 
+xo?(s).(C'(x , X!,y , yi, it, yi)) 
+y 1 1(s).(C'(x , xi, y , Vi,u, x )) 


C"(x , xi, y , yi,u, v) «- xi?(s).y \(s).(C'{x Q , Xi,y , yi,u, v)\u\) 
+y ?(s).x 1 l(s).(C'(x ,x 1 ,yo,yi,u,v)\ul) 
+u7.vl(s).(C(x a ,x 1 ,yo,y 1 ,u)) 

A crossing process has four ports xq , x\ , t/o , 2/1 and a hidden synchronizer u. 
Each port has a partner port, linked as shown in the diagram (note the relationship 
to Conway's ±1 tangles [H>|). For example, the first behavior (indicated by the first 
term of the summand) is that the process listens at port xi for a signal s (which 
will come, if at all, via the wiring process). Having heard s, the signal is passed 
directly to the port yo where the signal is then broadcast via the wiring process. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

Then the process alerts the hidden synchronizer u that a signal has been passed 
between the ports, while concurrently preparing itself for further signal processing. 
The second summand represents a signal passing along the same strand in the 
opposite direction. The third and fourth summands are similar to the first two, 
except that before passing any received signal to its partner port, the process waits 
for a signal from the synchronizer u before allowing the signal to pass, while still 
allowing a signal to pass between x\ and yo if the synchronizer has not yet been 
alerted. So the role of u is that of a traffic controller who gives priority to traffic 
over the route between x\ and yo, mimicking an over-crossing. 

4.2. Wirings 

As an illustration of the expressive power of the formalism, taken together with the 
short description of the process calculus in the next section, the definitions below 
fully equip the interested reader to verify that wire processes are lossless, infinite 
capacity buffers. 

W(x,y) <— [y n m)(Waiting(x,n,rn)\Waiting(y,m,n)) 
Waiting(x,c,n) <— xl{v).{i> m)(Cell(n,v,m)\Waiting(x,c 7 m)) 

+c?(w).c?(c).Ready(x, c, n, w) 
Ready{x 1 c, n, w) 4— xl{v).(v m)(Cell(n, v, m)\Ready(x, c, m, w j) 
+xl(w).Waiting(x, c, n) 
Cell(c,v,n) 4- c!(w).c!(n).0 

The ports x and y in which W is parameterized may be intuitively considered 
splice points in the knot diagram. We adopt this terminology in the sequel. 

One may well wonder why perfect buffers are chosen to represent wires. For 
example, the following process intuitively captures a notion of wire. 

Relay(x, y) := x?(s).yl(s). Relay <{x, y) + yl(s).x\(s).Relay(x, y) 

The problem is one of composition. Foreshadowing the method of proof, in the 
sequel we will need to compose wires and crossings and have the result act as a 
wire. For example, if W(x, y) represents a candidate for wire behavior, to model 
the first Rcidemeister move we have a demand that 

W{y ,yi) ~ {v x xi w w 1 )(W(y , w )\(v u)C(x ,xi,w ,wi,u)\W(x ,xi)\W(yi,w 1 )) 

Again, the reader may verify that while this is true of buffers, it is not true of 
the Relay process defined above. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

4.3. An example: the trefoil knot as a process 

The above intuitions are illustrated with an example, showing one way to represent 
the trefoil knot as a process. Following the schema above, the process encoding of the 
trefoil knot is a parallel composition of three crossing circuits with a wiring harness 
whose design ensures that the crossing circuits are connected to each other in a 
way that respects the knot diagram. Additionally, we make each synchronization 
channel local to each crossing via a restriction on that channel. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

[3i] = (v ...v 5 )(v u )C(vo 7 v 1 ,v 2 ,v 3 ,u ) 
\W(v 2 ,v 7 )\W(v 3 ,v 6 ) 
\{v ui)C(v 4 ,v 5 ,v e ,v 7 ,ui) 
\W(v 4 ,v 9 )\W(v 5 ,v 8 ) 

\(U U2)C(V8,VQ,V W ,VU,U 2 ) 

\W(v w , v )\W(vu,vi) 

4.4. The distinguishing power of dynamics 

In summary, to each knot K, the encoding associates an invariant \K\ , an expression 
in a calculus of message-passing processes via an encoding of a diagram of the knot. 
More precisely, given the set of knot diagrams K and the set of processes modulo 

structural equivalence P (see section 4.5 ), the encoding induces a map, [— ] : K — >• P. 
Most importantly, the notion of equivalence of knots coincides perfectly with the 
notion of equivalence of processes, i.e. bisimulation (written here and in the sequel 
~). Stated more formally, 

Theorem 4.2 (main). 

Ki~K* ^ ~ [#- 2 ]. 

In particular, in contrast to other invariants, the alignment of process dynamics 
with knot characteristics is what enables the invariant identified here to be perfectly 
distinguishing. As discussed below, among the other beneficial consequences of this 
alignment is the ability to apply process logics, especially the spatial sub-family of 
the Hennessy-Milner logics, to reason about knot characteristics and knot classes. 

We see moreover the possibility of a deeper connection. As mentioned in the 
previous section, bisimulation has turned out to a powerful proof technique in the 
theory of computation adaptable to a wide range of situations and admitting a 
number of potent up-to techniques [59] . One of the central aims of this research is 
to broaden the domain of applicability of bisimulation-based proof methods. 

4.5. The syntax and semantics of the notation system 

Having bootstrapped an intuitive account of the target calculus via the encoding, 
we now summarize a technical presentation of this calculus. The typical presenta- 
tion of such a calculus follows the style of giving generators and relations on them. 
The grammar, below, describing term constructors, freely generates the set of pro- 
cesses, V. This set is then quotiented by a relation known as structural congruence, 
yielding the set P mentioned above in the type signature of the map constituting 
the encoding. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

4.5.1. Process grammar 


M,N::=0 \ x.A \M + N A ::= (x)P \ [x]P 


P, Q::=N\ P\Q \X(y) | (rec X{x).P){y) \ (v x)P 

Note that x denotes a vector of names of length \x\. In the encodings for knots, 
crossings and wires given above we adopted the following standard abbreviations. 

xl{y).P:=x.{y)P x\(y).P := x.[y\P X(y) <- P := (y)(rec X($).P)(y) 

U^P i :=P Q \...\P n . 1 

4.5.2. Structural congruence 

Free and bound names and alpha-equivalence. At the core of structural 
equivalence is alpha-equivalence which identifies process that are the same up to a 
change of variable. Formally, we recognize the distinction between free and bound 
names. The free names of a process, J-M(P), may be calculated recursively as 

J7V(0) := 

TM{x7{y).P) := {x}U (TAf(P)\{y}) TAf(x!(y).P) := {x} U {y} U FM{P) 
TN{P\Q) := TN{P) U FN{Q) TN{P + Q) := TN{P) U FN{Q) 
FN{{v y)P) := FN{P) \ {y} 
J-AA((rec X(x).P)(y)) := {y} U FN{P) \ {x} 

The bound names of a process, BJV(P), are those names occurring in P that 
are not free. For example, in x7(y).0, the name x is free, while y is bound. 

Definition 4.3. Then two processes, P,Q, are alpha-equivalent if P = Q{y/x} 
for some x G BN{Q),y G BAf(P), where Q{y/x} denotes the capture-avoiding 
substitution of y for x in Q. 

Definition 4.4. The structural congruence [56j , =, between processes is the least 
congruence containing alpha-equivalence, satisfying the abelian monoid laws (as- 
sociativity, commutativity and as identity) for parallel composition | and for 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

summation +, in addition to the following axioms: 

(vx)0 = (v x){v x)P = {v x)P (u x){v y)P = (v y)(u x)P 

P\(v x)Q = {v x)(P\Q), if xg FN{P) 

(rec X(x).P)(y) = P{y/x}{(rec X(x).P)/X} 

4.5.3. Operational semantics 

Finally, we introduce the computational dynamics. What marks these algebras 
as distinct from other more traditionally studied algebraic structures, e.g. vector 
spaces or polynomial rings, is the manner in which dynamics is captured. In tradi- 
tional structures, dynamics is typically expressed through morphisms between such 
structures, as in linear maps between vector spaces or morphisms between rings. In 
algebras associated with the semantics of computation, the dynamics is expressed 
as part of the algebraic structure itself, through a reduction reduction relation typ- 
ically denoted by — >. Below, we give a recursive presentation of this relation for the 
calculus used in the encoding. 


yC\v = % \v\ = \A 

x.{y)P I x.(uv)[z\P^ {vv){P{z/y}\Q) 

Par Equiv New 

P -> P' P = P' P' -+Q' Q' = Q P -> P' 

P\Q->P'\Q P^Q (vx)P^(vx)P' 

We write =>■ for ->*, and P — > if 3Q such that P — > Q. 

In closing this summary, we take the opportunity to observe that it is precisely 
the dynamics that distinguishes this encoding. The equivalence that coincides with 
knot equivalence is a behavioral equivalence, i.e. an equivalence of the dynamics of 
processes in the image of the encoding. In a marked departure from Gauss codes or 
DT codes or Conway's "knotation," this facet of the encoding affords the conflation 
of notation scheme with invariant, providing a framework in which to establish the 
distinguishing power of the invariant and a language in which to express classes of 
knots as logical properties, as discussed in subsection [6] 

4.5.4. Bisimulation 

The computational dynamics gives rise to another kind of equivalence, the equiva- 
lence of computational behavior. As previously mentioned this is typically captured 
via some form of bisimulation. 

The notion we use in this paper is derived from weak barbed bisimulation [45] . 
We must introduce an "up to" (60] [48] strategy to deal with the fact that Rei- 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

demeister moves can not only introduce or eliminate crossings (see R\ R2), but 
"reorder" them (see R3). 

Definition 4.5. An agent B occurs unguarded in A if it has an occurence in A not 
guarded by a prefix x. A process P is observable at x, written here P \. x, if some 
agent x.A occurs unguarded in P. We write P JJ. x if there is Q such that P =>■ Q 
and Q I x. 

Definition 4.6. A barbed bisimulation is a symmetric binary relation S between 
agents such that P S Q implies: 

(1) If P -> P' then Q^Q' and P' S Q' , for some Q' . 

(2) If P I z, then Q |L x. 

P is barbed bisimilar to Q, written P ~ Q, if P 5 Q for a barbed bisimulation 5. 

4.5.5. Contexts 

One of the principle advantages of computational calculi like the 7r-calculus is a 
well-defined notion of context, contextual-equivalence and a correlation between 
contextual-equivalence and notions of bisimulation. The notion of context allows 
the decomposition of a process into (sub-)process and its syntactic environment, its 
context. Thus, a context may be thought of as a process with a "hole" (written □) 
in it. The application of a context M to a process P, written M[P], is tantamount 
to filling the hole in M with P. In this paper we do not need the full weight of this 
theory but do make use of the notion of context in the proof the main theorem. As 
will be seen, the Reidmeister moves amount to decomposing the representation of 
the knot into some collection of crossings or wires and the rest of the knot. 


M Ml M N ::= □ | x.M A | M M + M N M A ::= (x)M P | [x\M P 


M P ::= M N \ P\M P |(rec X(x).M P ){y) \ (u x)M P 

Definition 4.7 (contextual application). Given a context M, and process P, 
we define the contextual application, M[P] := M{PjO}. That is, the contextual 
application of M to P is the substitution of P for □ in M. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

Example 4.8. For example, if we take 

M 3l := (v ...v 5 )(u u Q )C(v , vi,v 2 ,v 3 , u ) 
\W(v 2 ,v 7 )\D 

\{v Ui)C(v 4 ,V 5 ,V 6 ,V 7 ,Ui) 

\W(v i7 Vg)\W(v 5 ,V 8 ) 

\{v U 2 )C(V8,Vg,Vi ,Vu,U 2 ) 

\W(v w , '^o)|W / («ii,wi) 

then l3 1 }=M 3l [W(v 3 ,v 6 )} 

5. Main theorem: proof sketch 

We have a couple of technicalities to dispatch. To motivate the first of these we wish 
to note that the arguments for the forward direction require some care. The aim is 
to capture the intuitive equivalence-preserving nature of the Reidemeister moves as 
corresponding bisimularity-preserving transformations on processes (in the image 
of the encoding) . Because of the encoding of crossing information of wires in terms 
of synchronization of signal-flow, we have to introduce "enough signal" to keep the 
knot "firing" , as it were, to establish that the process transformations corresponding 
to the knot transformations are bisimulation-preserving. Rather than seeing this 
extra condition as a weakness of the approach we submit that this feature provides 
evidence to our claim that the characterization of ambient isotopy of knots at work 
in this encoding is in terms of process dynamics. 

We will say that the encoding of a knot is alive as long as it is firing, i.e. the 
process is enabled to make a reduction step. If it ever ceases to push signal through, 
i.e. process cannot make a reduction step, then it is dead. 

We can ascertain an upperbound on initial signal that guarantees liveness of 
the encoding. Surely, the parallel composition of 2#(if) barbs, i.e. two barbs for 
each crossing, will guarantee the liveness of the encoding. More declaratively, we 
simply demand that [K] \init Signal be live before we are willing to admit it as a 
representation of the knot. 

Definition 5.1. More precisely, we will call the pair ([if], initSignal) alive 
if initSignal is an abstraction over a parallel composition of barbs, with 
\initSignal\ = we demand that for any vector of distinct names, v with 

M = 1 1-^1 1 an d any state, K' , such that \K\{v)\initSignal{v) => K' we have that 

Different crossing numbers mean different numbers of free names. Knots 
in the same isotopy class may have diagrams with different numbers of crossings. 
Different numbers of crossings lead to different aritics in the abstractions, so in 
interpreting these knots we haveto work to properly capture the notion of equiva- 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

lence. While the precise statement is somewhat technical, the intuition is simple: it 
is possible to find a common "interface" , i.e. argument list, between the two knots 
such that restricting to that argument list obtains bisimilar processes. 

Imagine (the processes that interpret) knots as programs housed in boxes with 
ports on the perimeter. Two knot diagrams Ki,i e {1,2}, from the same isotopy 
class may have different crossing numbers and thus their boxes have different num- 
bers #(Ki) of ports on the outside. We can find a number of ports, call it n, 
somewhere between the minimal crossing number of the isotopy class and the lesser 
of #{Ki) such that if - using restriction - we close off #(K\) — n ports on the 
first box and #(K 2 ) — n on the second we get two boxes that perform the same 
observable set of signal processing steps. 

Formally, suppose K\ ~ K 2 and let #Min(K) '■= min{#(K') : K' ~ K}. We 
assert that there is an n such that 4# Mi „(if 1 ) < n < 4 * min{#(Ki), #(K 2 )} and 
for any vector of names, v, with \v\ = n and v[i] 7^ v[j] •<=>■ i ^ j, there exists 
two vectors of names, Wi,w 2 , also all distinct, such that 

(y w^lK.Kv : w,) ~ {u w 2 )[K 2 \{v : w 2 ) 

with I toil = 4#(if l ) - n. 

Prime versus composite knots. Finally, we need to say a little about how we ob- 
tain a 7r-calculus expression for a given knot diagram. We use another bootstrapping 
procedure, beginning with another knot notation (Dowker-Thistlethwaite codes is 
used here) and exhibiting an algorithm for calculating a process expression from 
the chosen notation scheme. The reader will note that DT codes are unique only 
when restricted to the class of prime knots. It turns out that our encoding preserves 
knot composition. In fact, knot composition turns out to be a specialized form of a 
procedure, parallel composition + hiding, long-investigated in the process-algebraic 
setting. So, it is sufficient to demonstrate the encoding for prime knots. 

5.1. Forward direction. K x ~ K 2 =>- [-Ki] — [-K2] 

Strategy and intuitions. Since K\ ~ K 2 we know there is a sequence of Rei- 
demeister moves converting K\ to K 2 . Each move is proved to correspond to a 
bisimilarity-preserving transformation on a related process. We establish context 
and substitution lemmas and as a consequence obtain that the process operations 
corresponding to the Reidemeister moves preserve bisimularity. As noted above, a 
small amount of bookkeeping is required to iteratively apply these transformations 
to mirror Reidemeister moves as applied in a proof of ambient isotopy of two knots. 

We begin by observing that the intuition behind the Reidmeister moves is funda- 
mentally about performing local operations, i.e. on some subset of wires or crossings, 
while leaving the rest of the process unchanged. We interpret this notion of a "local 
operation" , say R, on a knot diagram K schematically as follows. 

• factor the process, \K\, as M[njCj|iTjWj] where niCi|IL;Wi encodes the set 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

Fig. 4. The figure illustrates a Reidemeister move of the first type as reflected in the context M 
of the 3i knot, as given in Ex. |4.8| 

of crossings or wires to be modified by R, i.e. the left side of the move to be 
performed, and M is the context representing the unchanged portion of the 

• letting R~^(K) (resp. R^(K)) denote the left-to-right (resp. right-to-left) ap- 
plication of the move R to K, then [R - *'^)] is calculated as M[n.j/(7|, |ILy/Wj-'], 
where HiiC' v \HjiWji are the processes interpreting the modified set of crossings 
or wires, i.e. the right side of the move to be performed. 

The mathematical content of these statements is that the encoding naturally 
extends to an encoding {Ri{L, R}J of the left and right hand sides of each Reidemeis- 
ter move such that {Kj = M[[R;Z]] (resp. M[[i?;R]]) and {Ri*(K)j = M[[R;R]] 
(resp. [R^~(-Fl)] = M[[RjX]]). Here, a picture really is worth a thousand words (see 
figure [5]) . 

478] taking M 3l 


be the encoding 
the strand corre- 

Example 5.2. For example, as in 
of Ri(3t,W(v3,ve)), the application of Ri to 3i at 
sponding to the wire process W(v 3 ,vq) is given by [Ri(3i, W(vs, v 6 ))j = 
[v x x\ y 2/i)M 3l [((v u)C(xo,x 1 ,yo,y 1 ,u)\W(xo,x 1 )\W{yo,v 3 )\W(y 1 ,v 6 ))}. See 
figure |4] 

A certain discipline is required in the extended encoding. To establish our sub- 
stitution and context lemmas we have to keep the interface (i.e. the ports in the 
process expression corresponding to the splice points) of the left and right hand 
sides of the R-move the same. So, for R\L and R2L we must restrict the ports that 
are not the splice points. One way to address this is to embed the restrictions into 
the encodings of R\L and R2L. Algebraically, 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

Fig. 5. Reidemeister moves as bisimilarity-preserving transformations. Cf. Fig.^ 

[i? 1 L](yO,yl) = 

(y x xi w Wi)(W(y , w ) 

\(p u)C(x ,xi,wo,wi,u)\W(x ,xi) 

\W( yi ,wi)) 

[i? 2 i](a;oo,a;oi,^io,^ii) = 
(y Voo, Voi, 2/io, t/ii, w 00 , tuoijtoio, u>ii)(W(xoo, u>oo)\W(xoi, t«oi) 

\(v u )C(wqo,w 01 , 2/00, 2/oi, wO) 

\W(y o,yu)\W(yoi,yio) 

\(v ui)C(wi , wn, 2/10, 2/n, wi) 

|W A (a;io,'u;io)|VF(a;ii,wii)) 

Keeping to the notion of equivalence outlined in the section above, however, it 
will be convenient to factor out the restrictions as in the example above. 

Lemma 5.3 (context). Vi € {1,2,3} if K\ ^ i^en //iere exists a context M 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

and (possibly empty) vector of distinct names w such that 

(y w)\K x \{v^w) = {vw)M\\R l L\\ 
\K 2 \ = M{lR t R]} 

Proof. This follows directly from the definition of the encoding. □ 

Lemma 5.4 (substitution). For all i e {1,2,3} RiL is bisimilar to RiR in the 
context of a live encoding. That is, if 

• \K\\initSignal is alive, and 

• {K\\initSignal = M[[i?,L]] 

for some context M then we can substitute [RiR] in its place without change of 
behavior, i.e. 

(vw)M[[RiL}] ~ M[lR t Rj] , Vi e {1,2,3} 

Proof. This follows from the definitions of \Ri{L, R}j plus the requirement that 
M derives from a live encoding. Even if one side has additional synchronizations, 
there is always enough signal to overcome spurious blocking. □ 

An immediate consequence of these two lemmas is 

Lemma 5.5 (1-step). if K\ can be derived from K 2 by application of one Reide- 
meister move, then 

[JfiKw) ~ (i/ w)\K 2 \(v:w) 

We are almost in a position to complete the proof of the forward implication. 
The next step is to show that you can iterate the performance of these bisimilarity- 
preserving transformations in a way that precisely mimics iterated application of 
Reidemeister moves. Because the moves R\ and R 2 change the number of crossings 
the number of ports in the interface of the (encoding of the) knot to which they 
are applied changes. This is the core issue in the formal statement of the theorem. 
Because the splice interface remains constant across the two sides of a Reidemeister 
move all one has to do is keep track of the ports to be hidden. The complete proof 
uses a case analysis of the composition of any two types of Reidemeister moves. 
We illustrate the analysis in the case of a simplifying (crossing-elimination) R\ step 
followed by a complicating (crossing-introducing) R 2 step. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

• The R\L — > R\R step means we have a context M such that 

{v x xi w Wi)[Xi](wo : x : x x : w : wi) 

= (y xo x l wo w^MllRrL}} 
~ MgR.Rj] 
= lK 2 j(vo). 

• The R2R — > R2L step means we have a context M' such that 

(u yoo ■■ ■ yn w Q0 ... wxi)lK a }{vi : y 00 : . . . : yn 

woo ■ ■ ■ ■ ■ wii) 
w n )M'[lR 2 L]\ 

= Voo ■ ■ ■ Vxx woo ■ ■ 
~ M'WR.R}] 

- [Km). 

• Since Vq,v{ are just lists of distinct names with \v^\ = Ip^JI = just pick 
Vq = v\. Dropping the subscript, we conclude 

[y xo x 1 w w^lKxjiv : x : x x : w ■ Wi) ~ 
(v yoo--- yn w 00 --- wn)[X 3 ](ul : y 00 : . . . : yn : w o ■ ■ ■ ■ ■ %) 

• Moreover, we have [-K2](i5) forming the shared core. 

The attentive reader might wonder how R3 works. Indeed, Perko pairs provide 
a key counter example to using restriction. This is where bisimulation really shows 
it's value - in the form of its flexibility. The outline follows the proof technique of 
bisimulation- up-to (in this case, up to context), found in |57j after noting that that 
there are two simple paths in the knot encoding between any given pair of distinct 

5.2. Reverse direction. K 1 ~ K 2 -t= [[i^i] ~ [[K2] 

We prove this by contradiction, assuming two knots in distinct isotopy classes with 
bisimilar images and arriving at absurdity. Not surprisingly, the argument in this 
direction is considerably less complicated as it is nonconstructive. 

Without loss of generality (by application of the lemmas of the forward direction 
as needed), we assume knots are given in minimal crossing diagrams. Due to this 
minimality, if the crossing numbers of these diagrams are different, then the number 
of free names (or arity of the abstractions interpreting the knots) in [ifi] differs 
from those in [-K2] -contradicting bisimilarity. Thus, the crossing numbers must be 
the same. 

Now we employ the form of the encoding: n'/Z 1 [C'(i)](...)|n™ ; r 1 W^(...)|W / (...) ~ 
n"r 1 [C , (j)](...)|n™r 1 l^ / (...)|W // (...). Notice that a consequence of sharing the same 
crossing number is that the crossing process part of the two encodings is iden- 
tical. Because bisimulation is a congruence this implies H^- 1 W(...)\W{...) ~ 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

WJ~qW' (...)\W (...). This says that the only difference can be in the "wiring har- 
nesses". Obviously, if any of these wires differ (up to a-equivalence), then there is 
a distinguishing barb, contradicting our assumption of bisimulation. Hence none of 
the wires differ, their respective sets of crossings are wired identically, which means 
the diagrams are identical. Thus, the knots are ambiently isotopic - a contradiction. 

6. Unlikely characters: spatial logic for knots 

Associated to the mobile process calculi are a family of logics known as the 
Hennessy-Milner logics. These logics typically enjoy a semantics interpreting for- 
mulae as sets of processes that when factored through the encoding outlined above 
allows an identification of classes of knots with logical formulae. In the context of 
this encoding the sub-family known as the spatial logics [3] [10] [E] are of particular 
interest providing several important features for expressing and reasoning about 
properties (i.e. classes) of knots. We hint here at how this may be done. 

6.0.1. Structural connectives 

The spatial logics enjoy structural connectives corresponding, at the logical level, to 
the parallel composition (P\Q) and new name {(v x)P) connectives for processes. 
As illustrated in the examples below, these connectives are extremely expressive 
given the shape of our encoding. 

6.0.2. Decideable satisfaction 

In [5] the satisfaction relation is shown to be decideable for a rich class of processes. 
It further turns out that the image of the our encoding is a proper subset of that 
class. This result provides the basis for an algorithm by which to search for knots 
enjoying a given property. 

6.0.3. Characteristic formulae 

In the same paper [5] , Caires presents a means of calculating characteristic formu- 
lae, selecting equivalence classes of processes up to a pre-specified depth limit on 
the support set of names. Composed with our encoding, this characteristic formula 
can be used to select characteristic formulae for knots. 

6.0.4. Spatial logic formulae 

The grammar below (segmented for comprehension) summarizes the syntax of spa- 
tial logic formulae. We employ illustrative examples in the sequel to provide an 
intuitive understanding of their meaning referring the reader to [8] for a more de- 
tailed explication of the semantics. 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 


A, B ::=T \ ->A \ A A B \ rj = rj' | | A\B \ x®A | Vx.A | Hx.A 


| a.A | X{u) | tiX{u).A a (x?(y)) \ (xl(y)) | (r) n ::= x | r 

6.1. Example formulae 
6.1.1. Crossing as formula. 

{j,C{x , Xi,y , y 1 ,u).{(x ?(z))((ul)(y 1 lz)C(x , xx, yo,yi,u)) 
A (yi^(z))((ul)(x lz)C(x Q , x-l, 2/0,2/1, «)) 
A (xi?(z))((u?) (y lz)C(x , xi,y , y\,u)) 
A (yo?(^))((w?)(2:i!z)C(:Eo,2i,?/o,yi,w))) 

The lexicographical similarity between the shape of this formulae and the shape 
of definition of the process representing a crossing reveals the intuitive meaning of 
this formulae. It describes the capabilities of a process that has the right to represent 
a crossing. For example it picks out processes that may perform an input on the 
port xq in its initial menu of capabilities. What differentiates the formula from the 
process, however, is that the crossing process is the smallest candidate to satisfy the 
formula. Infinitely many other processes - with internal behavior hidden behind this 
interface, so to speak - also satisfy this formula. Even this simple formula, then, can 
be seen to open a new view onto knots, providing a computational interpretation 
of virtual knots. 

Note that this formula is derived by hand. A similar formula can be derived 
by employing Caires' calculation of characteristic formula [8] to the process repre- 
senting a crossing. In light of this discussion, we let [CJ^xO, xl, yO, yl, u) denote 
a formula specifying the dynamics we wish to capture of a crossing. To guaran- 
tee we preserve the shape of the interface and minimal semantics we demand that 
[CJ^xO, xl, j/0, yl, u) C(a;0, xl, 2/0, yl, u) where C{xQ, xl, yO, yl, u) denotes the 
formula above. 

6.1.2. Crossing number constraints. 

The moral content of the context lemma (Lemma 5.3) is that the notion of "local- 
ity" in the Reidemeister moves is effectively captured by the parallel composition 
operator of the process calculus. This intuition extends through the logic. Given 
a formula, [CJ^xO, xl, yO, yl, u), we can use the structural connectives to specify 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

constraints on crossing numbers, such as at least n crossings, or exactly n crossings. 


K f n (xs,ys) := U^Hu.lCfl^(xsi,ysi,u)\T 


K $ n (xs, ys) := II "Zq 1 Hu.lCl$(xsi,ysi,u)\-i (Vx , y , x\ , y 1 , u. [C] ^ (x , Vo , xi , Vi , u) \ T) 

To round out this section, recall that the encoding of an n-crossing knot decom- 
poses into a parallel composition of n copies of a crossing process together with 
a wiring harness. To specify different knot classes with the same crossing number 
amounts to specifying logical constraints on the wiring harness. In the interest of 
space, we defer examples to a forthcoming paper. Suffice it to say that both the 
conditions "alternating knot" and "contains the tangle corresponding to 5/3" are 
expressible. For example, it is possible to calculate the characteristic formula of a 
process corresponding to the tangle 5/3 and conjoin it into the classifying formula 
via the composition connective of the logic. 

Finally, we wish to observe that it is entirely within reason to contemplate a 
more domain-specific version of spatial logic tailored to the shape of processes in 
the image of the encoding. Such a domain-specific logic would have a better claim 
to the title formal language of knot properties. 

7. Conclusions and future work 
7.1. Knotation system properties 

Rather than list the properties of section |2.2| and tick them off, as we may do, let 
us take a step back. In the end it is the act of calculating over knots - tabulat- 
ing, searching, making new ones from old - that places demands on the notation 
system used to represent them. These are the practical considerations that give 
rise to the properties listed in |2.2| Establishing the tight correspondence between 
processes in the image of the encoding and the knots they represent is ultimately 
in service of showing this is a reasonable proxy for knots because calculations on 
the representation have a correspondence to calculations on the domain. Moreover, 
the last few decades of logic in computer science has taught us that there is fidelity 
and then there is fidelity. It's one thing map elements of one domain to elements of 
another, but it's another to map the procedures of one domain (roughly, operations 
on elements) to the procedures of another. Whether one sees a demand like this 
through the lens of "functoriality" or through a correspondence of proofs (of say, 
ambient isotopy, in a proof system made of Reidmeister moves) and programs (that 
transform programs) , the practical side of the demand is about making calculation 
tractable, so that "local" operations in one domain correspond to "local" opera- 
tions in the other. This makes it possible to structure calculations in terms of the 
structure of the elements over which the calculations are being performed, which 
has far-ranging consequences on the complexity of calculation in the representative 

14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

domain. Of note, we have been careful to restrict attention to the image of the 
encoding. We do not, as of yet, have an effective characterization of processes that 
will decide whether or not a process is in the image of the encoding. This restriction 
notwithstanding, the image is the only system thus far proposed that does enjoy 
all of the properties listed, including possessing (actually, being) a language for 
classifying knots via logical properties. 

7.2. Knot queries 

The interest in knot tabulation coming from the physical sciences is a strong mo- 
tivation to investigate the design of a specialized form of spatial logic tailored to 
reasoning about processes in the image of this encoding. Specifically, the current 
authors are in the process of devising an executable knot query language that runs 
on top of a translation of spatial logic predicates to XQuery, the XML query lan- 
guage [?] [55]. In this application, a member, K, of an isotopy class [K]~ is stored 
as an XML document [[if]]xML- As the notation indicates, the document may 
be calculated from the process expression, {KJ. Pleasantly, all such documents will 
conform to an XML schema [I5J [55J that may be formally derived from the 

grammar for processes described in section 4.5.1 Thus, the mathematics extends 
to a formal specification of the software implementation of a "knot database" and 
the compositional nature of the specification makes tractable formal verification of 
the correctness of the software with regards to the specification. 

7.3. Braids, tangles, virtual knots, racks and quandles 

As may be seen from the encoding of the Reidcmcister moves, nothing in this 
approach restricts it to knots. In particular, the same techniques may be lifted to 
braids and tangles. More generally, Kauffman posits an intriguing new member to 
the knot family by virtualizing the crossings in a knot diagram |29j . We note that 
while we arrived at this encoding before becoming aware of Kauffman's work, that 
line of investigation is very much aligned to the guiding intuitions of the encoding 
presented here. Namely, the crossing circuit a priori could be any 7r-calculus process 
that respects the interface of the wiring circuit. We conjecture that many forms of 
virtualization may be faithfully interpreted as simulation. 

Moreover, it seems likely that the rack and quandle frameworks may be mirrored 
in the process calculus, as these structures can be used to model the action of the 
Reidemeister moves on a knot. The relation between this type of action and the 
dynamics of the process calculus presented here remains to be investigated. 

7.4. Other calculi, other bisimulations and geometry as behavior 

The astute reader may have noticed that the encoding described here is not much 
more than a linear notation for a minimal graph-based representation of a knot di- 
agram. In this sense, there appears to be nothing particularly remarkable about the 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

representation. Though expressed in a seemingly idiosyncratic way, the encoding is 
built from the same information that any freely downloadable program for calculat- 
ing knot polynomials uses routinely. What is remarkable about this representational 
framework is that it enjoys an independent interpretation as the description of the 
behavior of concurrently executing processes. Moreover, the notion of the equiv- 
alence of the behavior of two processes (in the image of the encoding) coincides 
exactly with the notion of knot equivalence. It is the precise alignment of indepen- 
dently discovered notions that often indicates a phenomena worth investigating. 

This line of thought seems particularly strengthened when we recall the ir- 
calculus is just one of many 'computational calculi' — the A-calculus being an- 
other paradigmatic example — that may be thought of as a computational dynam- 
ics+algebra and that virtually every such calculus is susceptible to a wide range of 
bisimulation and bisimulation up-to techniques |42j . As such, we see the invariant 
discussed here as one of many potential such invariants drawn from these relatively 
new algebraic structures. It is in this sense that we see it as a new kind of invariant 
and is the inspiration for the other half of the title of this paper. 

Finally, if the reader will permit a brief moment of philosophical reflection, we 
conclude by observing that such a connection fits into a wider historical context. 
There is a long-standing enquiry and debate into the nature of physical space. 
Using the now familiar signposts, Newton's physics — which sees space as an ab- 
solute framework — and Einstein's — which sees it as arising from and shaping 
interaction — we see this connection as fitting squarely within the Einsteinian 
Weltanschauung. On the other hand, unlike the particular mathematical framework 
of continuity in which Einstein worked out his programme, behavior and its implied 
notions of space and time are entirely discrete in this setting, built out of names 
and acts of communication. In this light we look forward to revisiting the now well- 
established connection between the various knot invariants such as the Kauffman 
bracket and quantum groups. Specifically, it appears that the kinematic picture of 
loop quantum gravity derived from spin networks can be faithfully encoded in a 
manner analogous to one used here to encode knots, but the process structure offers 
an account of dynamics somewhat different from spin foams [4] . 

8. Appendix: From DT-codes to processes 

What follows is an algorithm for calculating the u indexing function. Note that the 
function over can be implemented easily using the function 5, or the function sgn, 
described in section 2.1.6 Exercise for the reader: upgrade the algorithm so that 
wires are not duplicated during the process. 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

* *) 

* *) 

* Given types Knot and Wire, the omega function is typed as follows *) 

* omega : int -> (int -> int) -> (int -> int) -> Knot -> (Wire list) *) 

* With dt a table representing the Dowker-Thistlethwaite mapping *) 

* from odds to evens, and dti the inverse. The function keeps an *) 

* accumulator, acc, in which to collect the wires it calculates. *) 

* The function assumes helper functions C and x0,xl,y0,yl. C takes *) 

* and instance of type Knot and the odd index of the DT code and *) 

* returns the crossing. The other helpers are accessors of the ports *) 

* of the crossing. The algorithm visits every crossing and so *) 

* generates many wires more than once, which is why the accumulator *) 

* is updated with union rather than cons on the recursive calls. As *) 

* an exercise, modify the algorithm to avoid wire duplication. *) 

* *) 
* *) 

let omega i dt dti knot acc = 
if (i <= (numCrossings knot)) 

let ic = (2*i - 1) in 

(i+1) dt dti knot 
(union acc 

[ W(xl(C(knot,ic)) , 
(if (over dt ic-1) 

then yO(C (knot, ic-1) ) 
else yl(C(knot,ic-l)))) ; 
W(yO(C(knot,ic)) , 
(if (over dt ic+1) 

then xl(C (knot, ic+1) ) 
else xO(C(knot,ic+l)))) ; 
W(xO(C(knot,ic)) , 
(if (over dt (dti ((dt ic)-l))) 

then yO(C (knot, (dti ((dt ic)-l)))) 
else yl(C (knot, (dti ((dt ic)-l)))))); 
W(yl(C(knot,ic)) , 
(if (over dt (dti ((dt ic)+l))) 

then xl(C (knot, (dti ((dt ic)+l)))) 

else xO(C (knot, (dti ((dt ic)+l)))))) ])) 

else acc 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

Acknowledgments. The authors wish to thank Matthias Radestock for sugges- 
tions for coding wires, and early advocation of the wire-saturated form the final 
encoding took and his probing questions regarding proof strategies in earlier drafts 
of this paper. One of the co-author wishes to acknowledge his longstanding debt 
to Samson Abramksy for making so accessible his foundational insights into the 
Curry-Howard isomorphism. Additionally, the authors would like to thank the re- 
viewers of ICALP 2006 for their helpful comments on an earlier write up of these 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 


[1] Martin Abadi and Bruno Blanchet. Analyzing security protocols with secrecy types 

and logic programs. In POPL, pages 33-44, 2002. 
[2] Martin Abadi and Bruno Blanchet. Secrecy types for asymmetric communication. 

Theor. Comput. Set., 3(298):387-415, 2003. 
[3] Samson Abramsky. Algorithmic game semantics and static analysis. In SAS, page 1, 


[4] John C Baez. An introduction to spin foam models of quantum gravity and bf theory. 

LECT.NOTES PHYS., 543:25, 2000. 
[5] P. D. Bangert. Algorithmic Problems in the Braid Groups. PhD thesis, University 

College London, 2002. 

[6] Paul V. Biron and Ashok Malhotra. XML schema part 2: Datatypes second edition. 

W3C recommendation, W3C, October 2004. 

xmlschema-2-20041028 / . 
[7] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating 

sequential processes. J. Assoc. Comput. Mach., 31(3):560-599, 1984. 
[8] Luis Caires. Behavioral and spatial observations in a logic for the pi-calculus. In 

FoSSaCS, pages 72-89, 2004. 
[9] Luis Caires and Luca Cardelli. A spatial logic for concurrency (part i). Inf. Comput, 

186(2) :194-235, 2003. 

[10] Luis Caires and Luca Cardelli. A spatial logic for concurrency - ii. Theor. Comput. 

Set., 322(3):517-565, 2004. 
[11] Jorge A. Calvo, Kenneth C. Millett, Eric J. Rawdon, and Andrzej Stasiak, editors. 

Physical and numerical models in knot theory, volume 36 of Series on Knots and 

Everything. World Scientific Publishing Co. Pte. Ltd., Singapore, 2005. Including 

applications to the life sciences. 
[12] Jorge Alberto Calvo. Knot enumeration through flypes and twisted splices. J. Knot 

Theory Ramifications, 6 (6): 785-798, 1997. 
[13] Luca Cardelli. Brane calculi. In CMSB, pages 257-278, 2004. 

[14] A. Caudron. Classification des noeuds et des enlacements. Prepublication Math. 
d'Orsay, Orsay, France: Universite Paris-Sud, 1981. 

[15] J. H. Conway. An enumeration of knots and links, and some of their algebraic prop- 
erties. In J. Leech, editor, Computational Problems in Abstract Algebra (Proc. Conf, 
Oxford, 1967), pages 329-358. Pergamon, Oxford, 1970. 

[16] Vincent Danos and Cosimo Laneve. Core formal molecular biology. In ESOP, pages 
302-318, 2003. 

[17] C. H. Dowker and Morwen B. Thistlethwaite. Classification of knot projections. 

Topology AppL, 16(1):19-31, 1983. 
[18] David C. Fallside and Priscilla Walmsley. XML schema part 0: Primer second edition. 

W3C recommendation, W3C, October 2004. 

xmlschema-0-20041028 / . 
[19] Wan Fokkink, Rob van Glabbeek, and Paulien de Wind. Compositionality of 

Hennessy-Milner logic through structural operational semantics. In Fundamentals of 

computation theory, volume 2751 of Lecture Notes in Comput. Set., pages 412-422. 

Springer, Berlin, 2003. 
[20] Cedric Fournet, Fabrice Le Fessant, Luc Maranget, and Alan Schmitt. Jocaml: A 

language for concurrent distributed and mobile programming. In Advanced Functional 

Programming, pages 129-158, 2002. 
[21] Cedric Fournet, Georges Gontheir, Jean-Jacques Levy, Luc Maranget, and Didicr 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

Remy. A calculus of mobile agents. In Ugo Montanari and Vladimiro Sassone, editors, 
CONCUR 1996, volume 1119 of Lecture Notes in Computer Science, pages 406-421. 
Springer- Verlag, 1996. 

[22] Rusins Freivalds. Knot theory, Jones polynomial and quantum computing. In Math- 
ematical foundations of computer science 2005, volume 3618 of Lecture Notes in 
Comput. Sci., pages 15-25. Springer, Berlin, 2005. 

[23] C. A. R. Hoare. Communicating sequential processes. Prentice Hall International 
Series in Computer Science. Prentice Hall International, Englewood Cliffs, NJ, 1985. 
With a foreword by Edsger W. Dijkstra. 

[24] C. A. R. Hoare. Notes on communicating sequential systems. In Control flow and 
data flow: concepts of distributed programming (Marktoberdorf, 1984), volume 14 of 
NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., pages 123-204. Springer, Berlin, 

[25] C. A. R. Hoare. Algebraic specifications and proofs for communicating sequential 
processes. In Logic of programming and calculi of discrete design (Marktoberdorf, 
1986), volume 36 of NATO Adv. Sci. Inst. Ser. F Comput. Systems Set., pages 277- 
300. Springer, Berlin, 1987. 

[26] Jim Hoste. The enumeration and classification of knots and links. In Handbook of 
knot theory, pages 209-232. Elsevier B. V., Amsterdam, 2005. 

[27] Jim Hoste, Morwen Thistlethwaite, and Jeff Weeks. The first 1,701,936 knots. Math. 
Intelligencer, 20(4):33-48, 1998. 

[28] Allen L. Brown Jr., Cosimo Laneve, and L. Gregory Meredith. Piduce: A process 
calculus with native xml datatypes. In Mario Bravetti, Leila Kloul, and Gianluigi 
Zavattaro, editors, EPEW/WS-FM, volume 3670 of Lecture Notes in Computer Sci- 
ence, pages 18-34. Springer, 2005. 

[29] Louis Kauffman and Vassily Olegovich Manturov. Virtual knots and links, 2005. 

[30] T. P. Kirkman. The enumeration, description, and construction of knots of fewer 
than ten crossings. Trans. Roy. Soc. Edin., 32:281-309, 1885. 

[31] Cosimo Laneve and Gianluigi Zavattaro. Foundations of web transactions. In FoS- 
SaCS, pages 282-298, 2005. 

[32] Tomas Liko and Louis H. Kauffman. Knot theory and a physical state of quantum 
gravity. Classical Quantum Gravity, 23(4):R63-R90, 2006. 

[33] J.B. Listing. Vorstudien zur topologie. Gottingen Studien, 2:811-875, 1848. 

[34] C. N. Little. On knots, with a census to order 10. Trans. Conn. Acad. Sci., 18:374- 
378, 1885. 

[35] C. N. Little. Alternate ± knots of order 11. Trans. Roy. Soc. Edin., 36:253-255, 1890. 

[36] C. N. Little. Non-alternate ± knots. Trans. Roy. Soc. Edin., 39:771-778, 1900. 

[37] Charles Livingston. Knot Theory. Carus Mathematical Monographs. MAA, 1993. 

[38] Noah Mendelsohn, Henry S. Thompson, David Beech, and Murray Maloney. XML 
schema part 1: Structures second edition. W3C recommendation, W3C, October 

[39] Greg Meredith and Steve Bjorg. Contracts and types. Commun. ACM, 46(10):41-47, 

[40] L. Gregory Meredith and Matthias Radestock. A reflective higher-order calculus. 

Electr. Notes Theor. Comput. Sci., 141(5):49-67, 2005. 
[41] L.G. Meredith and Matthias Radestock. A reflective higher-order calculus. In Mirko 

Viroli, editor, ETAPS 2005 Satellites. Springer- Verlag, 2005. 
[42] R. Milner and D. Sangiorgi. Techniques of weak bisimulation up-to, 1992. 
[43] Robin Milner. A Calculus of Communicating Systems. Springer Verlag, 1980. 
[44] Robin Milner. Elements of interaction - turing award lecture. Commun. ACM, 

September 14, 2010 0:12 WSPC/INSTRUCTION FILE jktir 

36(l):78-89, 1993. 

[45] Robin Milner. The polyadic 7r-calculus: A tutorial. Logic and Algebra of Specification, 
Springer- Verlag, 1993. 

[46] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes. I, 

II. Inform, and Comput., 100(l):l-40, 41-77, 1992. 
[47] Robin Milner and Davide Sangiorgi. Barbed bisimulation. In ICALP, pages 685-695, 


[48] Damien Pous. Weak bisimulation up to elaboration. In Christel Baier and Holger 

Hermanns, editors, CONCUR, volume 4137 of Lecture Notes in Computer Science, 

pages 390-405. Springer, 2006. 
[49] Corrado Priami, Aviv Regev, Ehud Y. Shapiro, and William Silverman. Application 

of a stochastic name-passing calculus to representation and simulation of molecular 

processes. Inf. Process. Lett., 80(1):25-31, 2001. 
[50] Stuart Rankin and Ortho Flint. Enumerating the prime alternating links. J. Knot 

Theory Ramifications, 13(1):151-173, 2004. 
[51] Stuart Rankin, Ortho Flint, and John Schermann. Enumerating the prime alternating 

knots. I. J. Knot Theory Ramifications, 13(1):57-100, 2004. 
[52] Stuart Rankin, Ortho Flint, and John Schermann. Enumerating the prime alternating 

knots. II. J. Knot Theory Ramifications, 13(1):101-149, 2004. 
[53] R. C. Read and P. Rosenstiehl. On the gauss crossing problem. Proc. Fifth Hungarian 

Comb. Colloq., 1977. 

[54] Amitai Regev and Ehud Y. Shapiro. Cells as computation. In CMSB, pages 1-3, 

[55] Kurt Reidemeister. Knoten und Verkettungen. Math. Z., 29(l):713-729, 1929. 

[56] David Sangiorgi and David Walker. The -K-Calculus: A Theory of Mobile Processes. 

Cambridge University Press, 2001. 
[57] Davide Sangiorgi. On the proof method for bisimulation (extended abstract). In 

MFCS, pages 479-488, 1995. 
[58] Davide Sangiorgi. Bisimulation in higher-order process calculi. Information and Com- 
putation, 131:141-178, 1996. 
[59] Davide Sangiorgi. Bisimulation: From the origins to today. In LICS, pages 298-302. 

IEEE Computer Society, 2004. 
[60] Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up to" . In 

CONCUR, pages 32-46, 1992. 
[61] Robert G. Scharein. Interactive Topological Drawing. PhD thesis, Department of 

Computer Science, The University of British Columbia, 1998. 
[62] Jerome Simeon, Denise Draper, Ashok Malhotra, Peter Fankhauser, Mary 

Fernandez, Michael Rys, Philip Wadler, and Kristoffer Rose. XQuery 1.0 and 

XPath 2.0 formal semantics. Candidate recommendation, W3C, June 2006. 
[63] P.G. Tait. On knots, i, ii, iii. In Scientific Papers, volume 1, pages 273-347. Cambridge 

University Press, Cambridge, 1898. 
[64] Pawel T. Wojciechowski and Peter Sewell. Nomadic pict: Language and infrastructure 

design for mobile agents. In ASA/MA, pages 2-12, 1999.